S. Krtchman, R. Raz; "The surprise examination paradox and the second incompleteness theorem"
URL
著者
モチベーション
memo
Abstrakt
We give a new proof for Godel's second incompleteness theorem, based on Kolmogorov complexity, Chaitin's incompleteness theorem, and an argument that resembles the surprise examination paradox. We then go the other way around and suggest that the second incompleteness theorem gives a possible resolution of the surprise examination paradox. Roughly speaking, we argue that the flaw in the derivation of the paradox is that it contains a hidden assumption that one can prove the consistency of the mathematical theory in which the derivation is done; which is impossible by the second incompleteness theorem.
端折って説明すると
$ Tは十分に強い体系とする．$ T \vdash \mathrm{Con}_Tで「$ Tは$ T自身の無矛盾性を証明出来る」を表す．
$ Tは「月曜日から金曜日のどこかでテストをやることは出来る」という事実を証明できる．
$ T \vdash \mathrm{Con}_Tならば，「金曜日にテストは出来ない」すなわち「遅くとも木曜日までには抜き打ちテストを行う」という事実を証明できる．
$ T \vdash \mathrm{Con}_Tならば，「木曜日にテストは出来ない」すなわち「遅くとも水曜日までには抜き打ちテストを行う」という事実を証明できる．
…
$ T \vdash \mathrm{Con}_Tならば，「月曜日にテストは出来ない」すなわち「遅くとも日曜日までには抜き打ちテストを行う」という事実を証明できる．
ところが，日曜日に抜き打ちテストをやることは出来ない．
なぜなら日曜日は月曜日から金曜日のどこかではないから．
結論として，$ T \vdash \mathrm{Con}_Tなら，$ Tは「月曜日から金曜日のどこかでテストをやることは出来ない」という事実を証明できる．
合わせると，
$ T \vdash \mathrm{Con}_Tなら，
「月曜日から金曜日のどこかでテストをやることは出来る」が$ Tで証明できる
「月曜日から金曜日のどこかでテストをやることは出来ない」が$ Tで証明できる
他方，$ Tは無矛盾なので，定義より
「$ A」と「$ Aでない」が同時に$ Tで証明できるということはありえない．
ここから，$ Tが無矛盾なら$ T \vdash \mathrm{Con}_Tとすることは出来ない，
すなわち「$ Tは無矛盾なら$ T自身の無矛盾性を証明出来ない」という結論が導かれる．
準備
もとの論文だとどう考えても計算が合わないので色々修正している
が，おれが間違っている可能性も全然ある
適当な万能計算機$ \mathcal{U}をひとつ固定する．
Kolmogorov複雑度$ K(x)は$ \mathcal{U}で$ xを出力するプログラムの中で最短の長さを持つプログラムの長さとする． プログラムの個数について
$ n \ge 1とする．
$ nbitのバイナリ列は$ 2^n種類存在する．
4bitのバイナリ列は$ 16 = 2^4個存在する．
$ \tt 0000,0001,0010,0011
$ \tt 0100,0101,0110,0111
$ \tt 1000,1001,1010,1011
$ \tt 1100,1101,1110,1111
それぞれを2進数表記された自然数として見ると$ 0,\dots,15の16種類ある．
$ nbitの自然数は$ 2^n種類存在する．
$ nbit未満のバイナリ列は高々$ 2^n-1個しか存在しない．
4bit未満のバイナリ列は$ 15 = 2^4-1個存在する．
$ \tt 000,001,010,011,100,101,110,111
$ \tt 00,01,10,11
$ \tt 0,1
$ \varepsilon
なおこのような$ \varepsilonを認めないのなら$ 2^n - 2個になるが，議論に支障はない．
それぞれをプログラムとして見ると
$ nbit未満のプログラムは高々$ 2^{n}-1個しか存在しない．
例えば，もし$ \mathcal{U}がプログラムコードを2進数の数と見て，+1する．（$ \varepsilonの場合$ 0とする）ような最もシンプルな計算機であった場合…
$ \mathcal{U}(\mathtt{\varepsilon}) = 0 ,~ \mathcal{U}(\mathtt{0}) = 1,~ \mathcal{U}(\mathtt{1}) = 2
$ \mathcal{U}(\mathtt{00}) = 3 ,~ \mathcal{U}(\mathtt{01}) = 4,~ \mathcal{U}(\mathtt{10}) = 5,~ \mathcal{U}(\mathtt{11}) = 6
$ \mathcal{U}(\mathtt{000}) = 7 ,~ \mathcal{U}(\mathtt{001}) = 8,~ \mathcal{U}(\mathtt{010}) = 9,~ \mathcal{U}(\mathtt{011}) = 10
$ \mathcal{U}(\mathtt{100}) = 11 ,~ \mathcal{U}(\mathtt{101}) = 12,~ \mathcal{U}(\mathtt{110}) = 13,~ \mathcal{U}(\mathtt{111}) = 14
すると$ 15だけ余る．
どんな万能計算機であったとしても，鳩の巣原理より1つは確実に余る 少なくとも1つの4bitの自然数（0 ~ 15）に対して，4bit未満のプログラムを割り当てることが出来ないのである．
その自然数に対しては，4bit以上のプログラムを割り当てる他に道は無い．
これを言い直すとこうなる
任意の$ n \ge 1について，$ nbitの自然数$ xで$ K(x) \ge nとなる$ xが存在する．
プログラムの個数について2
同じ議論の未満を以下に変えたものを考えよう．ここでは$ n \ge 0とする．
$ n+1bitの自然数は$ 2^{n+1}種類存在する．
$ nbit以下のプログラムは高々$ 2^{n+1} - 1個しか存在しない．
したがって
任意の$ n \ge 1について，$ nbitの自然数$ xで$ K(x) > nとなる$ xが存在する．
$ K(x) > nになっている点に注意．（$ \geでない）
十分に強力な無矛盾な理論を$ Tとする．
任意の$ xに対して「$ K(x) > L」が$ Tでは証明できないような，十分に大きな整数$ Lが存在する
remark:
この定理は以下のように書いたほうが見通しが良い．
任意の$ xに対し$ T \nvdash K(x) > Lであるような$ Lが存在する．
remark:
$ Tで証明できないのは「任意の$ xに対して$ K(x) > L」ではない．すなわち
$ T \nvdash \forall_x.\lbrack K(x)>L \rbrackであるような$ Lが存在する
ではない！
Chaitinの不完全性定理とその帰結
上の議論より，$ Lbitの自然数$ xで$ K(x) > Lとなる$ xが存在する．
すなわち，$ K(x) > Lが正しいような$ xは存在する．
しかし$ Lの定義より，その正しさは証明できないのである．
すなわち，$ \mathcal{N} \models K(x) > Lであるのに$ T \nvdash K(x) > L．
なお$ Lbitの自然数というのは具体的には$ 0 \leq x < 2^{L}-1である．
重要な注意
任意の$ n \ge 1, xについて$ K(x) \le nであることは証明が出来る．
任意の$ n\ge1,xに対して$ T \vdash K(x) \leq n
上の議論より$ nbit以下のプログラムというのは高々$ 2^{n+1}-1個しかない．
$ 2^{n+1}-1個のプログラムを全部列挙してそれぞれ計算する
もし$ xを出力するプログラムがあったなら少なくとも$ K(x) \leq nである．
実際には$ xを出力するプログラムの中で最も小さなもののサイズを$ K(x)とすれば良い．
もし一つもなかったのなら，少なくとも$ K(x) > nである．
直感的な説明
$ Tは十分に強い無矛盾な理論とする．$ \sf PAや$ \sf ZFCとする．
すなわち，任意の$ xに対して「$ K(x) > L」は$ Tで証明できないとする．
$ 0 \leq x \leq 2^L - 1のうち，$ K(x) > Lであるような$ xの数を$ mとする．
上の議論より，$ 1 \leq mである．（少なくともそういった$ xは一つ存在する．）
$ m = 1だと仮定する．
実際に$ K(x_1) > Lである数を$ x_1 \in \{0,\dots,2^{L}-1\}とする．
現時点では，これはわからない．
$ x_1以外の他の数（$ 2^L - 1個ある）を$ y \in \{0,\dots,2^{L}-1\}\setminus \{x_1\}とする．
これらも，現時点ではどれなのかはわからない．
一方で，定義より$ K(y) \le Lである．
任意の$ zについて，$ K(z) \le Lであることは証明できる．
$ 2^{L}個の自然数$ z \in \{0,\dots,2^{L}-1\}全てに対して$ K(z) \le Lかどうかを試してみる．
$ m = 1であるので，$ K(z) \not\leq L，すなわち$ K(z) > Lな$ zが1つ出てくるはずである．
その$ zこそが$ x_1である．
以上の議論より，$ x_1は$ K(x_1) > Lであることが証明されてしまった．
この議論がもし$ T上で出来たとする（実際に出来る）
ところが，$ K(x_1) > Lであることは$ Tで証明出来なかった筈で…
$ Tは無矛盾と仮定したので，$ T \vdash \sigmaかつ$ T \nvdash \sigmaであることはありえない．
よってこの議論は破綻する．$ m \neq 1．
したがって，$ 2 \leq mである．少なくともそういった$ xは2つ存在する．
$ m = 2だと仮定すると，$ m = 1での議論と全く同じ様に議論が破綻する
よって，$ m \neq 2であることが示される．
したがって，$ 3 \leq mである．しかし$ m = 3と仮定すると…
同じことを延々とやると，いずれ$ 2^{L}-1 \leq mであることが示され，そして$ m \neq 2^{L}-1であることが示される．
よって$ 2^L - 1 < mであることが証明される．
ところが$ 0 \leq x < 2^{L}-1なのでどれだけ大きくとも$ m \leq 2^{L}-1である．
あれ？
実際には$ m \leq 2^{L}-1である（なければならない）のでこの議論は何かが狂っている
形式的に言うと…
Def
$ x \in \{ 0,\dots,2^L-1 \}は$ 0 \leq x \leq 2^L -1の略記とする．
$ x \in \{ 0,\dots,2^L-1 \} \setminus \{y_1,\dots,y_n\}は$ 0 \leq x \leq 2^L -1 \land \bigwedge^n_{i=1}x \neq y_iの略記とする．
もちろん，$ \sf PAでは$ \inというものはない（定義しなければ）のでこのような記法になっているが，$ \sf ZFCとかならむしろ左のほうが正しい記法である．
$ \exists^D_{y_1,\dots,y_n}.は任意の$ y_i,y_jが条件を満たし，かつ$ y_i \neq y_jを表すとする．
互いに相違な$ y_1,\dots,y_nが存在する，の意味．
こうしないと$ y_1,\dots,y_nが重複した場合に$ n個になってくれない．
引き続き$ Tは十分に強い無矛盾な体系とする．
ここでは，$ \mathrm{Pr}_T(\ulcorner A \urcorner)で$ Aが$ Tで証明可能を表すとする．
本来なら数項$ \overline{\ulcorner A \urcorner}と明示しなければならないが，余りにも煩雑になるため省略する．
また$ Aの論理式の中で実際には数項として表現しなければならないものも，適当に省略するとする．
任意の論理式$ A,Bについて
D1. $ T \vdash \varphi$ \implies$ T \vdash \mathrm{Pr}_T \left(\ulcorner A \urcorner\right)
D2. $ T \vdash \mathrm{Pr}_T \left( \ulcorner A \to B \urcorner \right) \to \left( \mathrm{Pr}_T \left( \ulcorner A \urcorner \right) \to \mathrm{Pr}_T \left( \ulcorner B \urcorner \right) \right)
D3. $ T \vdash \mathrm{Pr}_T\left( \ulcorner A \urcorner\right) \to \mathrm{Pr}_T\left(\ulcorner\mathrm{Pr}_T\left(\ulcorner B \urcorner\right)\urcorner\right)
$ Tの無矛盾性を表す文を$ \mathrm{Con}_T \equiv \lnot\mathrm{Pr}_T(\ulcorner 0 = 1 \urcorner)と定める．
次の事実は使っても良いものとする．
$ T \vdash \mathrm{Con}_T \to \forall_{ x \in \{ 0,\dots,2^L-1 \}}.\left\lbrack \lnot\mathrm{Pr}_T\left(\ulcorner K(x) > L \urcorner\right) \right\rbrack
Lem 2. 形式化された「Kolmogorov複雑度が$ L以下であることは$ Tで証明可能」という事実
$ T \vdash \forall_{y \in \{ 0,\dots,2^L-1 \}}.\left\lbrack (K(y) \leq L) \to \mathrm{Pr}_T\left(\ulcorner K(y) \leq L \urcorner\right) \right\rbrack
Cor 3.
$ T \vdash \mathrm{Con}_Tなら，$ T \vdash \forall_{ x \in \{ 0,\dots,2^L-1 \}}.\left\lbrack \lnot\mathrm{Pr}_T\left(\ulcorner K(x) > L \urcorner\right) \right\rbrack
proof:仮定$ T \vdash \mathrm{Con}_T及び，Lem 1とMPより
$ mを上と同様に，$ 0 \leq x \leq 2^L - 1のうち$ K(x) > Lであるような$ xの数とする．
Lem 4
$ T \vdash m \leq 2^{L}-1
remark:
繰り返しになるが，実際には最大でも$ m \leq 2^{L}-1である．
この事実は$ Tで証明可能である．
Lem 5
$ T \vdash m \ge 1
remark
Lem 6
$ T \vdash \mathrm{Con}_Tなら，任意の$ 1 \leq i \leq 2^{L} - 1に対して，$ T \vdash (m \ge i + 1)
proof
帰納法で示す．
$ T \vdash m \ge 1はLem4
$ T \vdash (m \ge i)と仮定し，$ T \vdash (m \ge i+1)を示す．
1. $ T \vdash (m=i) \to \exists^D_{y_1,\dots,y_{2^L-1-i} \in \{ 0,\dots,2^L-1 \}}.\left\lbrack \bigwedge^{2^L-1-i}_{j=1}K(y_j) \leq L \right\rbrack
2. $ T \vdash (m=i) \to \exists^D_{y_1,\dots,y_{2^L-1-i} \in \{ 0,\dots,2^L-1 \}}.\left\lbrack \bigwedge^{2^L-1-i}_{j=1} \mathrm{Pr}_T\left(\ulcorner K(y_j) \leq L \urcorner\right) \right\rbrack
1とLem2より
3. $ T \vdash (m \ge i) \to \left( \left( \bigwedge^{2^L-1-i}_{j=1} K(y_j) \leq L \right) \to (K(x) > L) \right)
$ mの定義より．ここで$ x,y_1,\dots,y_{2^L-1-i}とは
任意の相違なる$ y_1,\dots,y_{2^L-1-i} \in \{ 0, \dots, 2^{L}-1\}
任意の$ x \in \{0,\dots,2^L-1\} \setminus \{y_1,\dots,y_r\}
4. $ T \vdash \mathrm{Pr}_T\left( \ulcorner m \ge i \urcorner \right) \to \left( \left( \bigwedge^{2^L-1-i}_{j=1} \mathrm{Pr}_T\left(\ulcorner K(y_j) \leq L \urcorner \right) \right) \to \mathrm{Pr}_T\left( \ulcorner K(x) > L \urcorner \right) \right)
5. $ T \vdash \left( (m = i) \land \mathrm{Pr}_T\left( \ulcorner m \ge i \urcorner \right) \right) \to \exists_{x \in \{0,\dots,2^L-1\}}.\left\lbrack \mathrm{Pr}_T\left( \ulcorner K(x) > L \urcorner \right) \right\rbrack
6. $ T \vdash \mathrm{Pr}_T(\ulcorner m \ge i \urcorner)
仮定$ T \vdash (m \ge i)とD1より．
7. $ T \vdash (m=i) \to \exists_{x \in \{0,\dots,2^L-1\}}.\left\lbrack \mathrm{Pr}_T\left( \ulcorner K(x) > L \urcorner \right) \right\rbrack
5と6より
8. $ T \vdash \forall_{x \in \{0,\dots,2^L-1\}}.\left\lbrack \lnot\mathrm{Pr}_T\left( \ulcorner K(x) > L \urcorner \right) \right\rbrack \to \lnot(m=i)
7の対偶
9. $ T \vdash \lnot(m=i)
8と仮定$ T \vdash \mathrm{Con}_T及びCor3より
10. $ T \vdash (m > i)
9と仮定より．
11. $ T \vdash (m \ge i + 1)
10より．
Cor 7
$ T \vdash \mathrm{Con}_Tなら，$ T \vdash (2^L - 1 < m)
proof: Lem5で$ i = 2^L-1の場合について．
Cor 8
$ T \vdash \mathrm{Con}_Tと仮定する．
1. Lem 4より$ T \vdash m \leq 2^{L}-1
2. Cor7より$ T \vdash 2^L - 1 < m
3. 1,2より$ T \vdash 0 = 1相当のものが証明される．
4. 3とD1より$ T \vdash \mathrm{Pr}_T\left( \ulcorner 0 = 1 \urcorner \right)
5. 4について，$ \mathrm{Con}_Tの定義より$ T \vdash \lnot\mathrm{Con}_T
6. しかし$ Tの無矛盾性より$ T \vdash \sigmaかつ$ T \vdash \lnot\sigmaであることはありえない．この議論は破綻する．
7. したがって$ T \vdash \mathrm{Con}_Tではない，すなわち，$ T \nvdash \mathrm{Con}_T！
$ Tが無矛盾なら，$ T \nvdash \mathrm{Con}_T
大雑把に言えば数学の理論における無矛盾性を証明可能としてしまうような仮定を暗黙に含んでしまっている点にある
Question
先生の「来週テストをやる」という告知を形式化するとどうなるのか？
驚き(Surprise)と知識(Knowledge)という概念の形式化が重要な点である
準備
やはり$ Tは十分に強い理論とする
$ \{1,\dots,5\}は日に対応する.
$ mをテストが行われる日とする．
形式化.1
「来週抜き打ちテストをやる，テストがいつ行われるかは当日になるまでわからない」
来週抜き打ちテストをやる
$ m \in \{1,\dots,5\}に相当．
これはまあまあ自明
テストがいつ行われるかは当日になるまでわからない
知るという概念を証明可能という概念に置き換えることが出来るとしよう． メモ: 論文はタイトルが間違っている?
上の論文はかなり古く，1998年の調査論文がある
これに基づいて置き換えると
on the night before the exam you will not be able to prove, using this statement, that the exam is tomorrow
試験の前の日に，この告知を用いて，明日テストであることは証明出来ない．
これと同値な対偶として，
任意の$ i \in \{1,\dots,5\}に対し，この告知を用いて$ (m \ge i) \to (m = i)ということが証明できれば，$ m \neq iである．
以上をまとめて形式化すると，先生の告知はこのように形式化される
$ S \equiv \lbrack m \in \{1,\dots,5\} \rbrack \land \bigwedge_{i \in \{1,\dots,5\}}\left\lbrack \mathrm{Pr}_{T,S}\left(\ulcorner m \ge i \to m = i \urcorner\right) \to (m \neq i ) \right\rbrack
$ \mathrm{Pr}_{T,S}(\ulcorner A \urcorner)
$ T上での論理式$ Sによる，$ Aの証明可能性を意味する論理式である
論理式$ Sから，$ Aの$ Tでの証明のGödel数$ wが存在が帰結することを言う？ SnO2WMaN.icon文がメチャクチャすぎてfrom the Formula $ Sがどこにかかっているのかわからない！
$ \mathrm{Pr}_T(\ulcorner S \urcorner) \to \mathrm{Pr}_T(\ulcorner A \urcorner) なのか？
$ \mathrm{Pr}_{T+S}(\ulcorner A \urcorner)かもしれない…
分析してみよう
$ m \ge 5だとすると$ m \in \{1,\dots,5\}より$ m = 5が導かれる．
したがって$ \mathrm{Pr}_{T,S}\left(\ulcorner m \ge 5 \to m = 5 \urcorner\right)である
ここでは$ Sがどうであれ常識的な算術の（$ Tでの）推論で導かれるので，実際には$ \mathrm{Pr}_{T}\left(\ulcorner m \ge 5 \to m = 5 \urcorner\right)と言えるかもしれない
すると$ Sの定義より，$ m \ne 5である．
$ Sより$ m \in \{1,\dots,4\}である．
上の議論より「$ Sより$ m \ne 5である」が言えたので，
$ \mathrm{Pr}_{T,S}\left(\ulcorner m \ge 4 \to m = 4 \urcorner\right)である．
$ m \ge 4なら$ m =4か$ m = 5であり，$ m = 5は$ Sに由来して棄却されるので
すると$ Sの定義より$ m \ne 4が証明される．
同じ様にやってれば$ m \ne 3,2,1となり，$ m \notin \{1,\dots,5\}となる．
よって$ Sは自己矛盾（$ S \to \bot）するのである．
$ Sは自己矛盾するというのは，矛盾しているのは教師の告知であることを意味する
しかし本当にこの形式化はあっていたのか？
すなわち，知っている = 証明可能であるの前提は正しいのか？
仮に$ Sの形式化がこれで正しいとしたら$ Sを用いて何でも証明可能である
例えば
生徒は，火曜日の夜に$ Sを用いれば水曜日にテストがあることを証明できる
ここから，生徒は水曜日にテストがあることを知っていると言えるのか？
これに対してはNoと言える．
同様に木曜日と金曜日にテストがあることも証明できるから．
知っている $ \iff 証明可能であるドクトリンはおかしい．
「知っている$ \implies証明可能」に基づいて，先生の告知を$ Sとして形式化したのは非常に直感的ではある．
しかし，
「証明可能$ \implies知っている」はかなり疑わしい．
$ Sで証明可能であることが，知っていることを導かない．
故に$ Sの形式化は本当に正しいものであったと言えるのか？
形式化.2
もう一回，火曜日に起こりうる可能性について考え直してみよう
1. 火曜日の夜，生徒は水曜日にテストがあることを証明できない．
2. 火曜日の夜，生徒は水曜日にテストがあることを証明できる．しかし同時に，木曜日と金曜日にテストがありうることも証明出来る．
実際には，この可能性は体系が矛盾している場合にだけ発生する．
言い換えれば，この可能性は体系の矛盾性と同値である．
3. 火曜日の夜，生徒は水曜日に，そして水曜日にだけ，テストがあることを証明できる．
木曜日と金曜日にテストがあることは証明出来ない．
直感的には，可能性3だけが「テストが水曜日にあると実際知っている」と同じであると思うだろう．
すなわち次のドクトリンが成り立つ
テストがある曜日に行われることを知っている
$ \iff テストがある曜日に行われることが証明可能でなおかつ，テストがその曜日以外に行われることは証明できない．
これに基づいて再び先生の告知を形式化してみよう
任意の$ i \in \{1,\dots,5\}に対し，
この告知を用いて$ (m \ge i) \to (m = i)ということが証明できて，
なおかつ$ i以外では$ (m \ge i) \to (m = i)ということが証明できないのならば，
すなわち$ (m \ge i) \to (m = j)となる$ j \neq iが存在しないのならば
$ m \neq iである．
$ S \equiv \lbrack m \in \{1,\dots,5\} \rbrack \land \newline \bigwedge_{i \in \{1,\dots,5\}}\left\lbrack \left( \mathrm{Pr}_{T,S}\left(\ulcorner m \ge i \to m = i \urcorner\right) \land \bigwedge_{j \in \{1,\dots,5\}, j \neq i } \lnot\mathrm{Pr}_{T,S}\left(\ulcorner m \ge i \to m = j \urcorner\right) \right) \to (m \neq i ) \right\rbrack
それでは分析してみましょう！
$ m \ge 5とする
$ m \in \{1,\dots,5\}より$ m = 5なので$ \mathrm{Pr}_{T,S}\left(\ulcorner m \ge 5 \to m = 5 \urcorner\right)である．
あるいはこれには$ Sは関連しないので$ \mathrm{Pr}_{T}\left(\ulcorner m \ge 5 \to m = 5 \urcorner\right)
ところがさっきとは違い，ここから直ちに$ m \neq 5は帰結しない
なぜならある$ j \neq 5で$ \mathrm{Pr}_{T}\left(\ulcorner m \ge 5 \to m = j \urcorner\right)である可能性があるため
しかしその可能性は$ T + Sの矛盾性を引き起こしうる
例えば$ j = 4とかにすると$ m = 5でかつ$ m = 4になる
これを形式化すると
$ \mathrm{Con}_{T+S} \to (m \neq 5)
ただし，$ \mathrm{Con}_{T+S} \equiv \lnot\mathrm{Pr}_{T+S}\left( \ulcorner 0 = 1 \urcorner \right)
$ T+Sの無矛盾性を表現している．
なので，$ m \neq 5は帰結しないのである
形式化.1と同様に行くのならば，$ \mathrm{Pr}_{T,S}\left( \ulcorner m \ge 4 \to m = 4 \urcorner \right)がまず言えなければならない．
しかし，$ Sでは$ m \in \{1,\dots,4\}が導けない．
実際に導かれるのは，$ \mathrm{Con}_{T+S} \to m \in \{1,\dots,4\}である．
なぜなら$ \mathrm{Con}_{T+S} \to (m \neq 5)だから
よって，$ \mathrm{Pr}_{T,S}\left( \ulcorner m \ge 4 \to m = 4 \urcorner \right)が得られない．
実際に得られるものは$ \mathrm{Pr}_{T,S}\left( \ulcorner (\mathrm{Con}_{T+S} \land m \ge 4) \to m = 4 \urcorner \right)である．
ここまでの議論より，生徒は$ T + Sが無矛盾である，すなわち$ T + S\vdash \mathrm{Con}_{T+S}であると信じれば，金曜日にテストは行えないことが証明できる
もし信じれば，木曜日の夜に金曜日にテストがあることがわかってしまう
しかし，$ T + Sの無矛盾性は決して証明できない（$ T + S \nvdash \mathrm{Con}_{T+S}）のだから，
$ mは決定できないのである．
SnO2WMaN.iconここの議論はなんかちゃんと理解出来てる気がしない
最後の議論
$ Sの自己言及性を祓う
すなわち$ \mathrm{Pr}_{T,S}の$ Sを祓う
Gödel数$ a,bについて，
$ a \rightsquigarrow bという表記で論理式$ E_a \to E_bを表すことにする．
$ \mathrm{Sub}(a,b)は
$ aが自由変数を1つもつ論理式$ E_a\lbrack x\rbrackのGödel数であったとき
$ xに$ b（の数項）を代入することで得られる文Gödel数を表すものとする．
すなわち，$ \mathrm{Sub}(a,b) = \ulcorner E_a(b) \urcornerである
Gödel数$ v_{i,j} \coloneqq \ulcorner m \ge i \to m = j \urcornerとする．
$ Q(x) \equiv \lbrack m \in \{1,\dots,5\} \rbrack \land \newline \bigwedge_{i \in \{1,\dots,5\}}\left\lbrack \left( \mathrm{Pr}_{T}\left(\ulcorner \mathrm{Sub}(x,x) \rightsquigarrow v_{i,i} \urcorner\right) \land \bigwedge_{j \in \{1,\dots,5\}, j \neq i } \lnot\mathrm{Pr}_{T}\left(\ulcorner \mathrm{Sub}(x,x) \rightsquigarrow v_{i,j} \urcorner\right) \right) \to (m \neq i ) \right\rbrack
そして最後に，文$ S \equiv Q(\ulcorner Q \urcorner)とするのである．
$ \mathrm{Sub}(\ulcorner Q \urcorner,\ulcorner Q \urcorner) = \ulcorner Q(\ulcorner Q \urcorner)\urcorner = \ulcorner S \urcornerであるので，
$ S \equiv \lbrack m \in \{1,\dots,5\} \rbrack \land \newline \bigwedge_{i \in \{1,\dots,5\}}\left\lbrack \left( \mathrm{Pr}_{T}\left(\ulcorner \ulcorner S \urcorner \rightsquigarrow v_{i,i} \urcorner\right) \land \bigwedge_{j \in \{1,\dots,5\}, j \neq i } \lnot\mathrm{Pr}_{T}\left(\ulcorner \ulcorner S \urcorner \rightsquigarrow v_{i,j} \urcorner\right) \right) \to (m \neq i ) \right\rbrack
ここで$ \rightsquigarrowと$ v_{i,j}をもとに戻せば
$ S \equiv \lbrack m \in \{1,\dots,5\} \rbrack \land \newline \bigwedge_{i \in \{1,\dots,5\}}\left\lbrack \left( \mathrm{Pr}_{T}\left(\ulcorner S \to (m \ge i \to m = i) \urcorner\right) \land \bigwedge_{j \in \{1,\dots,5\}, j \neq i } \lnot\mathrm{Pr}_{T}\left(\ulcorner S \to (m \ge i \to m = j) \urcorner\right) \right) \to (m \neq i ) \right\rbrack
ここにおいて，$ \mathrm{Pr}_{T,S}の$ Sは祓われ，$ \mathrm{Pr}_Tのみを使う自己参照的な文が結実した！
メモ
SnO2WMaN.icon